To resolve the problems on description and proof of semantic property preservation in Model-Driven Software Development (MDSD), a formal approach was proposed for software architecture model on the basis of type category theory and process algebra. The semantic constraints of component specifications which should be kept through model transformation, were deeply analyzed and discussed. From the view of diagram structure, port and configuration constraints, external behavior and component substitutability, the problem of property preservation was described, and the corresponding criteria was built at the same time. The framework provides a guidance for the definition of model transformation rules, and provides the basis to verify the correctness of model transformation as well as to analyze the effect of model transformation. The application research shows that, the approach enhances semantic description capabilities of component model, and can be used as an effective supplement for existing software modeling method.